M1, M2:msga{i:l}. ma-compatible{i:l}(M1; M2)  Prop{i'} 

latex

Definitions	x:A. B(x), t  T, Prop, M1 || M2, P & Q, M1 ||decl M2, 1of(t), 2of(t), State(ds), Valtype(da;k), A & B, x. t(x), MsgA, x(s), P  Q
Lemmas	fpf-compatible wf, Id wf, id-deq wf, Knd wf, Kind-deq wf, fpf-cap wf, fpf-join wf, subtype-fpf2, subtype-fpf-cap-void, fpf-sub-join-left, fpf-sub-join-right, ma-state wf, locl wf, top wf, subtype rel function, subtype rel dep function, subtype rel self, subtype-fpf-cap-top, pi1 wf, pi2 wf, product-deq wf, IdLnk wf, rcv wf, idlnk-deq wf, subtype rel list, subtype rel product, msga wf